%%%%%%%%%%%%%%%%%%%%% chapter.tex %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% sample chapter
%
% Use this file as a template for your own input.
%
%%%%%%%%%%%%%%%%%%%%%%%% Springer-Verlag %%%%%%%%%%%%%%%%%%%%%%%%%%

\chapter{Discussion}
\label{discussion} % Always give a unique label
% use \chaptermark{}
% to alter or adjust the chapter heading in the running head

\section{Subset of C}

To simplify our proof of concept, we created a subset of C that
includes only a small subset of its features: variable declarations,
assignment statements, goto statements, and conditional goto
statements. Notably absent are function definitions, function
calls, control structures, structs, unions, and the standard library.

Variables have only one type (int) and arrays are strictly one-
dimensional. Most integer mathematical operations are included.

Although many language constructs are missing from our subset,
it is possible to duplicate the functionality of many of the missing
features with the included features. For example, a conditional
goto statement and a few goto statements can easily duplicate
an if statement exactly.

We do not claim to have analyzed the language in its entirety;
instead, we claim to have proven that a static analysis of a C-
like language can be done that soundly proves some programs
to be free of out-of-bounds array references and therefore
free of buffer overflow vulnerabilities.

\section{Algorithm}

Our static analyzer performs an abstract interpretation of a C
program; that is, it interprets the program, but gives up some
precision in order to guarantee termination. Instead of storing
values, the abstract interpreter stores the sign (or set of
possible signs) of a value. It also stores a set of axioms that
describe what is known about a variable.

Whenever a variable is assigned, all previously existing axioms
that include that variable must be eliminated. But a new axiom
is added that asserts that the value of the variable is the same
as the right-hand side of the assignment statement.

The abstract interpreter traverses all possible paths. In our
subset, this means that it follows the obvious code path for
declaration statements, assignment statements, and goto
statements. It follows {\i both} paths that might be taken at
a conditional goto: the path through the goto's target, where
control jumps when the condition is true and the path through
the succeeding statement, where control goes when the
condition is false. When traversing each of these paths, the
abstract interpreter adds an axiom that asserts what must
have been true to take the path: that the condition is true on
the target path and that it is false on the successive path.

If the axioms are ever unsatisfiable, the path is not valid and
execution along this path in the abstract interpreter can
terminate. It also terminates an execution path whenever it
finds a fixed point in the state space and whenever it reaches
the end of the program.

The algorithm terminates when all execution paths have
terminated.

\section{Implementation}
The first stages of our static analyzer are really preprocessing.
We lex and parse C code and then translate it into an AST

\section{Termination}

\section{Correctness}

%
